package tr.edu.ege.kipler.satisfiability.container;

import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.Set;

import tr.edu.ege.kipler.common.Copyable;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.syntax.WorldElement;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class PBox implements Copyable<PBox>, FormulaBase {
	private Set<WorldElement> formulas = new HashSet<WorldElement>();

	private boolean isSatisfiable = true;

	public boolean isSatisfiable() {
		return isSatisfiable;
	}

	public void add(WorldElement formula) throws UnsatisfiableException {
		formulas.add(formula);
		if (causesUnsatisfiability(formula)) {
			isSatisfiable = false;
			throw new UnsatisfiableException();
		}
	}

	public boolean contains(WorldElement formula) {
		return formulas.contains(formula);
	}

	/**
	 * @param conDef
	 * @throws UnsatisfiableException
	 */
	private boolean causesUnsatisfiability(WorldElement formula) {
		boolean result = true;
		WorldElement negFormula = formula.copy().toggleNegated();
		if (!formulas.contains(negFormula)) {
			result = false;
		}
		return result;
	}

	public Set<WorldElement> getFormulas() {
		return new LinkedHashSet<WorldElement>(formulas);
	}

	public PBox copy() {
		PBox pbox = new PBox();
		pbox.isSatisfiable = isSatisfiable;
		pbox.formulas = new HashSet<WorldElement>(formulas);
		return pbox;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			PBox other = (PBox) obj;
			return formulas.equals(other.formulas);
		}
		return false;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append("PBox");
		buffer.append(" = {");
		for (WorldElement f : getFormulas())
			buffer.append(f + ", ");
		buffer.delete(buffer.length() - 2, buffer.length());
		buffer.append("}");
		return buffer.toString();
	}

}
